View Javadoc

1   package joeq.Compiler.Analysis.IPA;
2   
3   import java.util.Iterator;
4   import joeq.Class.jq_Initializer;
5   import joeq.Class.jq_Method;
6   import joeq.Compiler.Analysis.FlowInsensitive.MethodSummary;
7   import joeq.Compiler.Analysis.FlowInsensitive.MethodSummary.ParamNode;
8   import joeq.Compiler.Analysis.IPSSA.IPSSABuilder;
9   import jwutil.util.Assert;
10  import net.sf.javabdd.BDD;
11  import net.sf.javabdd.BDDDomain;
12  import net.sf.javabdd.BDDFactory;
13  import net.sf.javabdd.TypedBDDFactory.TypedBDD;
14  
15  class ParameterAliasing {
16      /***
17       * Finds parameter aliases under different constexts.
18       * */
19      public static class ParamAliasFinder extends IPSSABuilder.Application {
20          PAResults _paResults            = null;
21          PA _r                           = null;
22          private boolean _verbose        = false;
23          private boolean _RECURSIVE      = true;
24          private int MAX_CONTEXT_PRINT   = 1;
25          private boolean _CONSTRUCTORS   = false;
26          private int _aliasedCalls       = 0;
27          
28          BDDDomain Z2 = null;
29           
30          public ParamAliasFinder() {
31              super(null, null, null);
32          }
33          public ParamAliasFinder(IPSSABuilder builder, String name, String[] args) {
34              super(builder, name, args);
35          }
36          
37          protected void initialize() {
38              _CONSTRUCTORS = !System.getProperty("paf.constructors", "yes").equals("no");
39              _RECURSIVE    = !System.getProperty("paf.recursive", "yes").equals("no");
40              _verbose      = !System.getProperty("paf.verbose", "yes").equals("no");
41              
42              Z2 = _r.makeDomain("Z2", _r.Z.varNum());
43          }
44      
45          protected void parseParams(String[] args) {}
46          
47          class ModifiableBoolean {
48              boolean _value;
49              
50              ModifiableBoolean(boolean value){
51                  this._value = value;
52              }
53              boolean getValue() {return _value;}
54              void setValue(boolean value) {this._value = value;}
55          }
56          
57          void visitMethod(jq_Method m){
58              //if(getBuilder().skipMethod(m)) return;
59              //if(m.toString().startsWith("java.")) return;
60              if(_verbose) {
61                  System.out.println("Processing method " + m.toString());
62              }
63              MethodSummary ms = MethodSummary.getSummary(m);
64              if(ms == null) return;
65              if(ms.getNumOfParams() < 2) return;
66              if(!_CONSTRUCTORS && m instanceof jq_Initializer) {
67                  return;
68              }
69              
70              _paResults = getBuilder().getPAResults();
71              _r = _paResults.getPAResults();
72   
73              // get formal arguments for the method
74              BDD methodBDD = _r.M.ithVar(_paResults.getMethodIndex(m));  // 
75              BDD params    = _r.formal.relprod(methodBDD, _r.Mset);      // V1xZ
76              //System.out.println("params: " + params.toStringWithDomains());
77              Assert._assert(_r.H1cset != null);
78              Assert._assert(_r.H1.set() != null);
79              Assert._assert(_r.Z.set() != null);
80              TypedBDD contexts =                                         // V1c
81                  (TypedBDD)params.relprod ( _r.vP, _r.V1.set().union(_r.H1cset).unionWith(_r.H1.set()).unionWith(_r.Z.set()) );
82              //System.out.println("contexts: \n" + contexts.toStringWithDomains());
83              //TypedBDD pointsTo = (TypedBDD)params.relprod(r.vP, r.V1cH1cset);
84              //System.out.println("pointsTo: \n" + paResults.toString(pointsTo, -1));
85              
86              /*** Iterate through all the relevant contexts for this method */            
87              int i = 0;
88              ModifiableBoolean printedInfo = new ModifiableBoolean(false);
89              long contextSize = (long)contexts.satCount(_r.V1cset);
90              boolean foundAliasing = false;
91              for ( Iterator contextIter = contexts.iterator(); contextIter.hasNext() && i < MAX_CONTEXT_PRINT; i++ ) {
92                  // for this particular context #
93                  TypedBDD context = (TypedBDD)contextIter.next();
94                  //System.out.println("context: \n" + context.toStringWithDomains());
95  
96                  Assert._assert(_r.vPfilter != null);
97                  TypedBDD pointsTo  = (TypedBDD)_r.vP.and(_r.vPfilter.id());   // restrict by the type filter
98                  TypedBDD t2 = (TypedBDD)params.relprod(pointsTo, _r.V1.set().union(_r.V1cset));
99                  pointsTo.free();
100                 pointsTo = t2;
101                 //t = (TypedBDD)t2.exist(_r.Z.set());
102                 
103                 //System.out.println("pointsTo 1: " + pointsTo.toStringWithDomains());
104                 if(_RECURSIVE) {
105                     pointsTo = (TypedBDD) calculateHeapConnectivity(pointsTo);
106                 }
107                 //System.out.println("pointsTo 2: " + pointsTo.toStringWithDomains());
108 
109                 //System.out.println("t: " + t.toStringWithDomains());
110 
111                 //t: H1xH1cxZ
112                 foundAliasing |= processContext(m, ms, pointsTo, context, printedInfo);
113             }
114             if(foundAliasing) {
115                 if ( contextSize > MAX_CONTEXT_PRINT ) {
116                     System.out.println("\t\t(A total of " + contextSize + " contexts) ");  
117                 }
118                 _aliasedCalls++;
119             }
120         }        
121         
122         public BDD calculateHeapConnectivity(BDD h1) {
123             BDD result = _r.bdd.zero();
124             result.orWith(h1.id());
125             BDD h1h2 = _r.hP.exist(_r.Fset);
126             for (;;) {
127                 BDD b = h1.relprod(h1h2, _r.H1set);
128                 b.replaceWith(_r.H2toH1);
129                 b.applyWith(result.id(), BDDFactory.diff);
130                 result.orWith(b.id());
131                 if (b.isZero()) break;
132                 h1 = b;
133                 //++heapConnectivitySteps;
134             }
135             h1h2.free();
136             
137             return result;
138         }
139         
140         /***
141          *  Process context #i in the set of contexts.
142          * */
143         boolean processContext(jq_Method m, MethodSummary ms, BDD t, TypedBDD context, ModifiableBoolean printedInfo){
144             boolean result = false;  
145 
146             TypedBDD pointsTo = (TypedBDD)context.relprod(t, _r.V1cset.union(_r.H1cset));   // H1xZ
147             //System.out.println("pointsTo: " + pointsTo.toStringWithDomains());
148             t.free();
149             
150             /*    
151             t = (TypedBDD)pointsTo.exist(_r.Z.set());
152             //System.out.println(t.satCount() + ", " + pointsTo.satCount());
153             int pointsToSize = (int)pointsTo.satCount(_r.H1.set().and(_r.Zset));
154             int projSize     = (int)t.satCount( _r.H1.set() );
155             if(projSize < pointsToSize) {
156                 if(!printedInfo.getValue()) {
157                     //printMethodInfo(m, ms);
158                     printedInfo.setValue(true);
159                 }
160                 ProgramLocation loc = new ProgramLocation.BCProgramLocation(m, 0);
161                 
162                 System.out.println("\tPotential aliasing in context calling " + 
163                         m.getDeclaringClass().toString() + "." + m.getName().toString() + "(" + loc.getSourceFile() + ":" + loc.getLineNumber() + ")");
164                 //System.out.println(pointsTo.toStringWithDomains() + ", " + t.toStringWithDomains());
165                 result = true;
166                 //b.applyWith(result.id(), BDDFactory.diff);
167             }
168             t.free();
169             */
170             BDDDomain Z1 = _r.Z;
171             
172             TypedBDD pointsTo2 = (TypedBDD) pointsTo.replace(_r.bdd.makePair(Z1, Z2)); 
173             
174             BDD notEq = Z1.buildEquals(Z2).not();
175             TypedBDD pairs = (TypedBDD)pointsTo.and(pointsTo2).and(notEq);
176             
177             System.out.println("pairs: " + pairs.toStringWithDomains());
178             
179             return result;
180         }
181         
182         void printMethodInfo(jq_Method m, MethodSummary ms) {
183             if(_verbose == false) {
184                 System.out.println("Processing method " + m + ":\t[" + ms.getNumOfParams() + "]");
185             }
186             
187             for(int i = 0; i < ms.getNumOfParams(); i++) {
188                 ParamNode paramNode = ms.getParamNode(i);
189                 System.out.print("\t\t");
190                 System.out.println("Param: " + paramNode == null ? "<null>" : paramNode.toString_long());
191             }
192             System.out.print("\n");
193         }
194         public void run() {
195             for(Iterator iter = getBuilder().getCallGraph().getAllMethods().iterator(); iter.hasNext();) {
196                 jq_Method m = (jq_Method)iter.next();
197             
198                 visitMethod(m);
199             }
200             if(_aliasedCalls > 0) {
201                 System.out.println("A total of " + _aliasedCalls + " aliased calls");
202             }
203         }
204     }
205 }